i:Id, d:InDecl(i), p:(IdLnkId). d(p)  Type 

latex

Definitions	x:A. B(x), InDecl(i), t  T, d(p), x. t(x), Prop, x(s)
Lemmas	fpf-cap wf, IdLnk wf, Id wf, fpf-trivial-subtype-set, ldst wf, pi1 wf, product-deq wf, idlnk-deq wf, id-deq wf, top wf, fpf wf